A, B:Realizer. A  B  R-Feasible(B)  R-Feasible(A) 

latex

Definitions

x:A. B(x), P  Q, t  T, Prop, SQType(T), {T}, AB, A, False, ij, R-Feasible(R), True, b, Rnone?(x1), x. t(x), true, false, if b t else f fi, P & Q, A  B, , Y, P  Q, P  Q, , Realizer, Unit, x(s), , , left  right, @loc x initially v:T, @loc only events in L change x:T, only events in L send on lnk with tag, @loc effect knd(v:T)  x := f State(ds) v , sends knd(v:T) on l:tagged(g,State(ds),v):dt, @loc precondition for a(v:T):P State(ds) v, @loc: k writes only members of L, @loc: k sends only on links in L, @loc: only members of L read x

Lemmas

nat wf, R-size wf, R-Feasible wf, R-sub wf, le wf, nat plus wf, es realizer wf, bool cases, Rnone? wf, bool sq, bool wf, eqtt to assert, iff transitivity, assert wf, bnot wf, not wf, eqff to assert, assert of bnot, nat properties, ge wf, unit wf, Id wf, Knd wf, IdLnk wf, fpf wf, decl-state wf, decl-type wf, true wf, false wf, Rplus? wf, R-size-decreases, Rplus-implies, Rplus-left wf, Rplus-right wf, R-sub-compat